Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	minus(minus(x))	→ x
2:	minus(x + y)	→ minus(minus(minus(x))) * minus(minus(minus(y)))
3:	minus(x * y)	→ minus(minus(minus(x))) + minus(minus(minus(y)))
4:	f(minus(x))	→ minus(minus(minus(f(x))))

There are 16 dependency pairs:

The approximated dependency graph contains 2 SCCs: {5-16} and {20}.

Consider the SCC {5-16}. The usable rules are {1-3}. By taking the AF π with π(minus) = π(MINUS) = 1 together with the lexicographic path order with precedence * ≈ +, the rules in {1-3} are weakly decreasing and the rules in {5-16} are strictly decreasing.

Consider the SCC {20}. There are no usable rules. By taking the AF π with π(F) = 1 together with the lexicographic path order with empty precedence, rule 20 is strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.06 seconds) --- May 4, 2006